g:OCMon, u, v, w:|g|. (v < w)  ((u * v) < (u * w)) 

latex

Up	groups 1
Definitions of Statement	Mon, AbMon, OMon, OCMon
Definitions	t  T, P  Q, x:A. B(x), x,y. t(x;y), , OMon, P & Q, x f y, A, Mon, AbMon, OCMon, x(s1,s2), P  Q, P  Q, False
Lemmas	ocmon wf, grp car wf, grp lt wf, grp op wf, grp le wf, assert wf, linorder wf, grp lt is sp of leq a, grp op preserves le, grp leq wf, ocmon cancel, grp leq weakening eq, grp leq antisymmetry